Nuprl Lemma : R-sub-self
11,40
postcript
pdf
C
:Realizer.
C
C
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
Lemmas
es
realizer
wf
,
R-sub-lemma1
origin
C:Realizer. C 
C C:Realizer. C C 
Tx:A. B(x)